Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures
Identifieur interne : 003169 ( Main/Exploration ); précédent : 003168; suivant : 003170Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures
Auteurs : Yannick Chevalier [France] ; Michael Rusinowitch [France]Source :
- Theoretical computer science [ 0304-3975 ] ; 2010.
Descripteurs français
- Pascal (Inist)
- Théorie décision, Analyse décision, Analyse limite, Multiplication, Décryptage, Algorithme, Théorie ensemble, Résolubilité, Contrainte, Trace, Opérateur borné, Informatique théorique, Union disjointe, Procédure décision, 68P25, 68Wxx, 03Exx, Protocole sécurité, Chiffrement, Protocole cryptographique.
English descriptors
- KwdEn :
- mix :
Abstract
Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication, abstract encryption/decryption. In this report we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.
Url:
Affiliations:
- France
- Grand Est, Lorraine (région), Midi-Pyrénées, Occitanie (région administrative)
- Nancy, Toulouse
- Université Toulouse III - Paul Sabatier
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000227
- to stream PascalFrancis, to step Curation: 000791
- to stream PascalFrancis, to step Checkpoint: 000168
- to stream Main, to step Merge: 003231
- to stream Hal, to step Corpus: 004952
- to stream Hal, to step Curation: 004952
- to stream Hal, to step Checkpoint: 002781
- to stream Main, to step Merge: 002F39
- to stream Main, to step Curation: 003169
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures</title><author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>IRIT, Team LiLac, Université Paul Sabatier</s1><s2>Toulouse</s2><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region">Occitanie (région administrative)</region><region type="old region">Midi-Pyrénées</region><settlement type="city">Toulouse</settlement></placeName><orgName type="university">Université Toulouse III - Paul Sabatier</orgName></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name><affiliation wicri:level="3"><inist:fA14 i1="02"><s1>Loria-INRIA Lorraine, Cassis Project</s1><s2>Nancy</s2><s3>FRA</s3><sZ>2 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">10-0147183</idno><date when="2010">2010</date><idno type="stanalyst">PASCAL 10-0147183 INIST</idno><idno type="RBID">Pascal:10-0147183</idno><idno type="wicri:Area/PascalFrancis/Corpus">000227</idno><idno type="wicri:Area/PascalFrancis/Curation">000791</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000168</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000168</idno><idno type="wicri:doubleKey">0304-3975:2010:Chevalier Y:symbolic:protocol:analysis</idno><idno type="wicri:Area/Main/Merge">003231</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00455290</idno><idno type="url">https://hal.inria.fr/inria-00455290</idno><idno type="wicri:Area/Hal/Corpus">004952</idno><idno type="wicri:Area/Hal/Curation">004952</idno><idno type="wicri:Area/Hal/Checkpoint">002781</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">002781</idno><idno type="wicri:doubleKey">0304-3975:2010:Chevalier Y:symbolic:protocol:analysis</idno><idno type="wicri:Area/Main/Merge">002F39</idno><idno type="wicri:Area/Main/Curation">003169</idno><idno type="wicri:Area/Main/Exploration">003169</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures</title><author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>IRIT, Team LiLac, Université Paul Sabatier</s1><s2>Toulouse</s2><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region">Occitanie (région administrative)</region><region type="old region">Midi-Pyrénées</region><settlement type="city">Toulouse</settlement></placeName><orgName type="university">Université Toulouse III - Paul Sabatier</orgName></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name><affiliation wicri:level="3"><inist:fA14 i1="02"><s1>Loria-INRIA Lorraine, Cassis Project</s1><s2>Nancy</s2><s3>FRA</s3><sZ>2 aut.</sZ></inist:fA14><country>France</country><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation></author></analytic><series><title level="j" type="main">Theoretical computer science</title><title level="j" type="abbreviated">Theor. comput. sci.</title><idno type="ISSN">0304-3975</idno><imprint><date when="2010">2010</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Theoretical computer science</title><title level="j" type="abbreviated">Theor. comput. sci.</title><idno type="ISSN">0304-3975</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algorithm</term><term>Bounded operator</term><term>Computer theory</term><term>Constraint</term><term>Cryptographic protocol</term><term>Decision analysis</term><term>Decision theory</term><term>Decryption</term><term>Encryption</term><term>Limit analysis</term><term>Multiplication</term><term>Security protocol</term><term>Set theory</term><term>Solvability</term><term>Trace</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Théorie décision</term><term>Analyse décision</term><term>Analyse limite</term><term>Multiplication</term><term>Décryptage</term><term>Algorithme</term><term>Théorie ensemble</term><term>Résolubilité</term><term>Contrainte</term><term>Trace</term><term>Opérateur borné</term><term>Informatique théorique</term><term>Union disjointe</term><term>Procédure décision</term><term>68P25</term><term>68Wxx</term><term>03Exx</term><term>Protocole sécurité</term><term>Chiffrement</term><term>Protocole cryptographique</term></keywords><keywords scheme="mix" xml:lang="en"><term>Cryptographic protocols</term><term>Dolev-Yao intruder</term><term>combination of decision procedures</term><term>equational theories</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication, abstract encryption/decryption. In this report we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li><li>Midi-Pyrénées</li><li>Occitanie (région administrative)</li></region><settlement><li>Nancy</li><li>Toulouse</li></settlement><orgName><li>Université Toulouse III - Paul Sabatier</li></orgName></list><tree><country name="France"><region name="Occitanie (région administrative)"><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name></region><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003169 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003169 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Pascal:10-0147183
|texte= Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures
}}
| This area was generated with Dilib version V0.6.33. |  |